$\forall$$A$,$B$:Type, $a$:EqDecider($A$), $b$:EqDecider($B$). union{-}deq($A$; $B$; $a$; $b$) $\in$ EqDecider($A$ + $B$)